\documentclass[a4paper]{article}
\usepackage[utf8x]{inputenc}
\usepackage{amssymb}

\begin{document}
\title{AAP - Trabajo Práctico 2: Análisis Dataflow \\ Detección de accesos ilegales a \emph{arrays}}
\date{\today}

\author{Bugni , Paulovsky , Perez (Grupo 2)}

\maketitle

\section{Ejercicio 1}

Se realizaron los siguientes cambios en el código para detectar posibles errores de referencias nulas:

\begin{itemize}
\item Agregamos soporte para parámetros que sean \textbf{objetos} arbitrarios. Hecho ese cambio la segunda función de \textbf{Class1.java} tira warnings por posibles parámetros \emph{Integer} \textit{null}.
\end{itemize}

\section{Ejercicio 2}

Para el desarrollo del chequeador de accesos a arrays nos basamos en los visitors del código del Ejercicio 1.
En las siguientes secciones detallamos las clases que desarrollamos en el contexto del análisis \emph{dataflow}.

\subsection{Reticulado}

\subsubsection{Intervalos}

Definimos un reticulado donde los elementos son vectores $[min,max]$ donde $min \in \mathbb{Z} \cup \{-\infty\}$ y $max \in \mathbb{Z} \cup \{\infty\}$. Para este fin definimos la clase \emph{Interval} que implementa
\begin{itemize}
\item operaciones aritméticas entre intervalos ($+,-,\times$; dejamos de lado la división por custiones de tiempo);
\item comparaciones básicas de intervalos ($=, \subset$)
\item operaciones de conjuntos básicas entre intervalos ($\cup,\cap, \smallsetminus$\footnote{En el caso de $\smallsetminus$ se devuelve, en caso de que el resultado sean dos intervalos disjuntos, uno sólo de ellos});
\item operaciones que devuelven un intervalo que representa a todos los números menores (resp. mayores) que el intervalo dado;
\item una operación auxiliar usada en la función de transferencia, que dados dos intervalos $i$ y $j$ y una relación binaria $\oplus$ ($=, \neq, <, \leq, >, \geq$), provee dos pares de intervalos $(i_t,j_t),(i_f,j_f)$ correspondientes a asumir como verdadera (resp. falsa) la relación binaria $i \oplus j$. Éstos son calculados en base a los intervalos de entrada.
\end{itemize}

\subsubsection{Operaciones de reticulado}

Con respecto a las operaciones de reticulado entre intervalos, definimos en la clase \emph{ArrayBoundsLatticeElement}

\begin{itemize}
\item como $\top$ al intervalo $[-\infty,\infty]$;
\item como $\bot$ al intervalo vacío;
\item como $i$ $asPreciseAs$ $j$ a la relación $i \subseteq j$; y 
\item como \emph{join} a la unión de dos intervalos en el menor que los contenga a ambos.
\end{itemize}

\subsection{PairLatticeElement}

Crystal provee el \emph{mapping TupleLatticeElement}, que utilizamos para relacionar variables con sus intervalos asociados. \emph{PairLatticeElement} es una extensión que incorpora un \emph{mapping} entre variables de array y variables temporales generadas en la representación TAC intermedia. 

Mantenemos esta información durante la transferencia para poder acceder en el análisis posterior a la información sobre la longitud de un determinado arreglo que está presente en las variables temporales y no se transfiere a la variable del arreglo original (dado que en el TAC las comparaciones se realizan siempre entre variables temporales).

El \emph{PairLatticeElement} define las mismas operaciones que \emph{ArrayBoundsLatticeElement}, redierccionando a ésta las operaciones, salvo en el caso del join que tiene además un paso extra donde comprueba si es necesario hacer \emph{widening}. 

\subsubsection{Estrategia de \emph{widening}}

Para hacer \emph{widening} mantenemos en un \emph{map} auxiliar un conteo de la cantidad de veces que hicimos \emph{join} del \emph{ForStatement} o \emph{WhileStatement} (subclases de \emph{ASTNode}) dado. Si el conteo supera el máximo arbitrario de 1000 iteraciones, procedemos a mirar qué variables cambiaron en el join y, comparando los límites de los intervalos, los extendemos a $-\infty$ (el mínimo) o a $\infty$ (al máximo) según corresponda. Esto nos provee convergencia aunque puede dar falsos positivos.

\subsection{Función de transferencia}

Definimos la función de transferencia como una extensión de la clase de Crystal \emph{AbstractTACBranchSensitiveTransferFunction}, por lo cual nuestro análisis se realiza sobre \emph{Three Address Codes} y es sensible a \emph{branching}. Esta función maneja como elementos del reticulado a objetos del tipo \emph{PairLatticeELement}.

Al comienzo todas las variables del análisis comienzan valiendo $\top$.

Entre las operaciones que realiza tenemos
\begin{itemize}
\item copia de intervalos entre variables;
\item adquisición del tamaño de un array creado dentro de la función visitada;
\item actualización del \emph{mapping} entre \emph{arrays} y variables temporales;
\item ejecución abstracta de operaciones aritméticas entre intervalos;
\item y resolución de comparaciones entre intervalos (utilizando la auxiliar de \emph{Interval} ya mencionada).
\end{itemize}

\subsection{Análisis de accesos a \emph{array}}

Al analizar los resultados del \emph{dataflow} se visita cada acceso a posición de array $arr[i]$ (tanto de lectura como escritura) y se comprueba 

\begin{itemize}
\item que $arr$ tenga algún intervalo definido distinto a $\bot$; en caso contrario, se informa una advertencia de posible acceso erróneo;
\item que el intervalo correspondiente a $i$ no se superponga con el intervalo $[-\infty,-1]$ ni con el intervalo correspondiente a $arr$; si además de superposición se verifica una contención se puede informar un error en lugar de una advertencia.
\end{itemize}

Estas reglas se explican porque para cada \emph{array} guardamos el intervalo de sus posibles longitudes; por lo que toda intersección no vacía entre éste y el intervalo de $i$ significa un posible acceso ilegal al \emph{array}. Dado que  comenzamos suponiendo que todas las variables son $\top$ ($[-\infty,\infty]$), si no aprendemos nada en el análisis \emph{dataflow} daremos advertencia en cada acceso a array ancontrado (pero no error).

\section{Ejercicio 3}

Haciendo pruebas sobre \textbf{Class2.java} tenemos los siguientes comentarios: 
\begin{itemize}
\item El análisis detectó como warnings a los accesos en \emph{SumArray1} y \emph{SumArray5}\footnote{Este falso positivo se debe al widening realizado, aunque lo detectamos como advertencia y no como error.}.
\item A pesar de funcionar como lo esperado, notamos que en \emph{SumArray4} el intervalo calculado para la variable $b$ es $[4,20]$ en lugar del esperado $[8,20]$. Notamos que el visitor de Crystal no está procesando correctamente expresiónes del tipo $ x = a + b + c + \dots$ (y es indistinto acá si $a,b$ y $c$ son variables o constantes) dado que sólo termina sumando las dos primeras. Por esto, la expresión $b = a + a + a + a$ termina valiendo $a + a$ lo cual es $[4,4]$ en ese punto del flujo.
\item El \emph{widening} en \emph{SumArray5} fue necesario porque al incrementar la variable $a$ dentro del $for$ no se llegaba al punto fijo. Comentando ese incremento o cambiándolo por algo como $a = i$ nos permitió alcanzar el punto fijo sin necesidad de hacer \emph{widening}.
\item Pudimos verificar el funcionamiento del $if$ jugando con los valores de $a$ y $b$ en \emph{SumArray2} \emph{SumArray4}. Cambiando a un valor erróneo en sola una de las ramas nos informa una advertencia, y haciéndolo en ambas nos informa un error.
\end{itemize}

\end{document}
